$\forall$$M$:MsgA, $k$:Knd, $x$:Id. ($\uparrow$$M$:$k$ may not read $x$) $\Leftarrow\!\Rightarrow$ ($\neg$$M$.rframe($k$ reads $x$))